COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Equations ({eq }), ({eq }) and ({eq }) can all be regarded as
C00004 ENDMK
C⊗;
Equations ({eq }), ({eq }) and ({eq }) can all be regarded as
axiom schemata in first order logic but containing a second
order functions %At%1.  Thus a sentence of first order logic
results from substituting a suitable functional for %At%1
and a suitable first order funtion for %Af%1 in ({eq }).
As long as we regard the schema as just a way of generating
a computable collection of first order formulas, there is
no reason to regard it as different in principle from a first
order schema.  However, we may conjecture that not every
collection of first order sentences that can be generated
by a second order schema can also be generated from a first
order schema.  There is a problem that not every second order
functional may be substituted for %At%1 in the schema; it has
to be continuous.  What this means in general is not clear.

Proving non-termination with finite approximation functions.